\begin{tabbing}
$\forall$\=${\it es}$:ES, $T$:Type, ${\it eq}$:EqDecider($T$), $v$:$T$, $x$:Id, $e$:\{$e$:E$\mid$ @loc($e$)($x$:$T$)\} ,\+
\\[0ex]${\it e'}$:\{${\it e'}$:E$\mid$ $e$ $\leq$loc ${\it e'}$  \& ($x$ after ${\it e'}$) = $v$\} , $a$:E.
\-\\[0ex]$e$ $\leq$loc $a$ 
\\[0ex]$\Rightarrow$ (($x$ after $a$) = $v$)
\\[0ex]$\Rightarrow$ $\forall$${\it e''}$$\in$[$e$,$a$).$\neg$(($x$ after ${\it e''}$) = $v$)
\\[0ex]$\Rightarrow$ ($a$ = next event in [$e$;${\it e'}$] after which $x$ = $v$)
\end{tabbing}